Inference at * 1 2 
Iof proof for Lemma eq atom eq false elim sqequal:

.....wf..... NILNIL

1. x : Atom
2. y : Atom
  (x =a y ~ ff)  Type 

latex

 by MemCD 

latex

 1: .....subterm..... T:t1:n

 1:   x =a y ~ x =a y
 2: .....subterm..... T:t2:n

 2:   ff ~ ff
 .

Definitions	t  T
Lemmas	atom sq